es:ES, dom:(E), e:E. sub-es-pred(es;dom;e)  (?{e:E| (dom(e))} ) 

latex

Definitions	x:A. B(x), t  T, sub-es-pred(es;dom;e), P  Q, T, True, , Y, if b then t else f fi , tt, ff, i  j , A  B, A, False, , , Unit, SWellFounded(R(x;y)), x:A. B(x), P  Q, P & Q,
Lemmas	es-locl-swellfnd, nat wf, es-E wf, bool wf, event system wf, le wf, es-locl wf, es-first wf, eqtt to assert, it wf, assert wf, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, es-pred wf, es-pred-locl, nat properties, ge wf